Nuprl Lemma : coprime_divisors_prod
2,24
postcript
pdf
a1
,
a2
,
b
:
. CoPrime(
a1
,
a2
)
a1
|
b
a2
|
b
a1
a2
|
b
latex
Definitions
P
Q
,
b
|
a
,
CoPrime(
a
,
b
)
,
x
:
A
.
B
(
x
)
,
t
T
,
P
Q
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
Prop
Lemmas
add
functionality
wrt
eq
,
mul
preserves
eq
,
coprime
bezout
id
,
coprime
wf
,
divides
wf
origin
a1, a2, b:
. CoPrime(a1,a2) 
a1 | b a2 | b a1
a2 | b a1, a2, b:. CoPrime(a1,a2) a1 | b a2 | b a1a2 | b Qx:A. B(x)
T
Q
x:A. B(x) Q